\begin{abstract}
Pattern matching is a powerful construct for conditional execution, and is
present in many programming languages, particularly in functional ones. The
number and complexity of patterns in a matching expression often grows quickly
as programs are written, and the task of checking the completeness or
disjointness of such an expression becomes tedious. Compilers can assist
programmers to some extent, but complex cases, such as the use of guards to
refine the patterns, are in general too difficult to deal with and are hence
treated very conservatively. As a result, no useful information can be gained
from the compilation process and programmers, once more, have to resort to
manual checking of their expressions.

In this project, we show how formal verification techniques can be used to
prove completeness or disjointess of a pattern matching expression with guards.
Our examples and results are based on the Scala programming language
\cite{Scala}, but we believe they can be extended to other languages with a
minimal amount of work. 
\end{abstract}

%\begin{keywords}
%pattern matching
%\end{keywords}
